\begin{tabbing}
ecl{-}es{-}halt(${\it es}$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then \=es{-}first{-}since(${\it es}$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)\+
\\[0ex]c$\wedge$ ($\uparrow$(${\it test}$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$))));$e_{1}$;$e_{2}$)
\-\\[0ex]else False
\\[0ex]fi );
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0) then False else ${\it ha}$($n$,$e_{1}$,$e_{2}$) fi 
\\[0ex]$\vee$ existse{-}between3(${\it es}$;$e_{1}$;$e_{2}$;$e$.(${\it ha}$(0,$e_{1}$,es{-}pred(${\it es}$; $e$))) $\wedge$ (${\it hb}$($n$,$e$,$e_{2}$))));
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then \=((${\it ha}$(0,$e_{1}$,$e_{2}$)) $\wedge$ existse{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.${\it hb}$(0,$e_{1}$,$e$)))\+
\\[0ex]$\vee$ ((${\it hb}$(0,$e_{1}$,$e_{2}$)) $\wedge$ existse{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.${\it ha}$(0,$e_{1}$,$e$)))
\-\\[0ex]else \=((${\it ha}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($b$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]else alle{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$(${\it hb}$($m$,$e_{1}$,$e$)))
\\[0ex]fi ))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($a$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]else alle{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$(${\it ha}$($m$,$e_{1}$,$e$)))
\\[0ex]fi ))
\-\-\-\\[0ex]fi );
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. ((${\it ha}$($n$,$e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($b$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]else alle{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$(${\it hb}$($m$,$e_{1}$,$e$)))
\\[0ex]fi ))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($a$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]else alle{-}between2(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$(${\it ha}$($m$,$e_{1}$,$e$)))
\\[0ex]fi )));
\-\-\\[0ex]$a$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then False
\\[0ex]else es{-}pstar{-}q(${\it es}$;$x$,$y$.${\it ha}$(0,$x$,$y$);$x$,$y$.${\it ha}$($n$,$x$,$y$);$e_{1}$;$e_{2}$)
\\[0ex]fi );
\\[0ex]$a$,$m$,${\it ha}$.${\it ha}$;
\\[0ex]$a$,$m$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0) then False else ${\it ha}$($n$,$e_{1}$,$e_{2}$) fi 
\\[0ex]$\vee$ if ($n$ =$_{0}$ $m$) then ${\it ha}$(0,$e_{1}$,$e_{2}$) else False fi );
\\[0ex]$a$,$l$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. ((${\it ha}$($n$,$e_{1}$,$e_{2}$)) $\wedge$ ($\neg$($n$ $\in$ $l$ $\in$ $\mathbb{N}$)))
\\[0ex]$\vee$ if ($n$ =$_{0}$ 0) then l\_exists($l$; $\mathbb{N}$; $m$.(${\it ha}$($m$,$e_{1}$,$e_{2}$))) else False fi ))
\-
\end{tabbing}